(declare-const r3 Real)
(declare-const r4 Real)
(declare-const r8 Real)
(declare-const r9 Real)
(assert (distinct 6104.0 (+ 345251.0 (- (- r4 345251.0)) (* 34.53599 r3 0.490565573 r3 345251.0)) r4 (* 34.53599 r3 0.490565573 r3 345251.0) (* r3 r3)))
(check-sat)
